package ch.epfl.lara.matcheck.verify;

import ch.epfl.lara.matcheck.ast.{Program,Tru,Formula,And}
import ch.epfl.lara.matcheck.verify.axioms._
import ch.epfl.lara.matcheck.util.FreshName

import ch.epfl.lara.matcheck.verify.spec.SpecVerifier

/**
 * <p>
 *	A class that by using the  AST of aprogram allow to extract axioms 
 *	for classes (e.g. subtyping relation, ...) and extractors 
 *	(that are encapsulated in an objects declarations). 
 *	Axiomes are returned as formulae.
 * </p>
 */
object AxiomsHolder extends  PredefAxioms
 	             with     ClassAxioms
                     with     ObjectAxioms
{

   private var collected: Boolean = false
   
   private var _axioms: Axiom = _
   private var _axiomsWithoutDomain: Axiom = _
   private var _domain: Axiom = _
   private var _constraint: Axiom = _
   
   def apply(program: Program) {
     if (collected) throw new Exception("Axioms have already been collected")
     
     val Program(_constraint,_domain,_objects,_classes) = program
     this._domain = _domain.getOrElse(Tru)
     this._constraint = _constraint.getOrElse(Tru)
     classesAxioms(_classes)
     objectsAxioms(_objects)
     _axiomsWithoutDomain = conjunction(predefined :: constraint :: classes :: extractors_results :: extractors_domains :: Nil) 
     _axioms = conjunction(domain :: _axiomsWithoutDomain  :: Nil)
     collected = true
   }
   
      
   def domain    : Axiom = _domain
   def constraint: Axiom = _constraint
   
   def axioms : Axiom =  _axioms
   def axiomsWithoutDomain: Axiom = _axiomsWithoutDomain 
}
  